(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(declare-fun xSquared () Int)
(declare-fun ySquared () Int)
(declare-fun zSquared () Int)
(declare-fun xSquaredPlusYSquared () Int)
(declare-const _a1 Bool)
(assert (=> _a1 (and (= xSquared (* x x)) (= ySquared (* y y)) (= zSquared (* z z)) (= xSquaredPlusYSquared (+ xSquared ySquared)) (> x 0) (> y 0) (> z 0) (= xSquaredPlusYSquared zSquared))))
(declare-const _a2 Bool)
(assert (=> _a2 (= 1 1)))
(check-sat)
